YES 0.912
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| (((!!) :: [a] -> Int -> a) :: [a] -> Int -> a) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| (((!!) :: [a] -> Int -> a) :: [a] -> Int -> a) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
The following Function with conditions
!! | (x : vv) 0 | = x |
!! | (vw : xs) n | |
!! | (vx : vy) vz | = error [] |
!! | [] wu | = error [] |
is transformed to
!! | (x : vv) yv | = emEm5 (x : vv) yv |
!! | (vw : xs) n | = emEm3 (vw : xs) n |
!! | (vx : vy) vz | = emEm1 (vx : vy) vz |
!! | [] wu | = emEm0 [] wu |
emEm1 | (vx : vy) vz | = error [] |
emEm1 | xv xw | = emEm0 xv xw |
emEm2 | vw xs n True | = xs !! (n - 1) |
emEm2 | vw xs n False | = emEm1 (vw : xs) n |
emEm3 | (vw : xs) n | = emEm2 vw xs n (n > 0) |
emEm3 | xy xz | = emEm1 xy xz |
emEm4 | True (x : vv) yv | = x |
emEm4 | yw yx yy | = emEm3 yx yy |
emEm5 | (x : vv) yv | = emEm4 (yv == 0) (x : vv) yv |
emEm5 | yz zu | = emEm3 yz zu |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
mainModule Main
| (((!!) :: [a] -> Int -> a) :: [a] -> Int -> a) |
module Main where
Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
mainModule Main
| ((!!) :: [a] -> Int -> a) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_emEm(:(zv30, zv31), Pos(Succ(zv400)), ba) → new_emEm(zv31, new_primMinusNat(zv400), ba)
The TRS R consists of the following rules:
new_primMinusNat(Succ(zv4000)) → Pos(Succ(zv4000))
new_primMinusNat(Zero) → Pos(Zero)
The set Q consists of the following terms:
new_primMinusNat(Zero)
new_primMinusNat(Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_emEm(:(zv30, zv31), Pos(Succ(zv400)), ba) → new_emEm(zv31, new_primMinusNat(zv400), ba)
The graph contains the following edges 1 > 1, 3 >= 3